$\forall$$D$:Dsys, $i$:Id. \{$m$:M($i$).Msg$\mid$ source(mlnk($m$)) = $i$\}  $\subseteq$r Msg($\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$))